Sandy Maguire is working on a book about type-level programming in Haskell with the working title of The Book of Types. It has prompted me to take stock of what I know about kinds.

Haskell 2010 Language Report

My starting point is the Haskell 2010 Language Report. It explains that the main forms of type expression are: type variables, type constructors, type application and a parenthesised type. A parenthesised type has the form (t) and is identical to the type t.

There are some built-in type constructors that have a special syntax, namely: the trivial type, (); the function type, (->), the list type, []; and the tuple types, such as (,) or (,,).

The function type (->) t1 t2 has the equivalent, and more traditional, form t1 -> t2.

The list type [] t has the equivalent form [t]. It denotes the type of lists with elements of type t.

The tuple type (,) t1 t2 has the equivalent form (t1,t2). It denotes the type of a tuple with the first component of type t1 and the second of type t2.

However, most type constructors are written as an identifer beginning with an uppercase letter. For example, Bool is a type constant (a nullary type constructor) and Maybe is a unary type constructor.

Type expressions are classified into kinds and kind inference checks the validity of type expressions.

The kind of all nullary type constructors is represented by the symbol *. For example, the kind of Bool is *.

The kind of type constructors that take a type of kind K1 and return a type of kind K2 is K1->K2. For example, the kind of Maybe is * -> *, as is the kind of [].

The kinds of (->) and (,) are * -> * -> *.

The kind of type constructors introduced by data or newtype is determined by kind inference. The kind of a type variable is determined by the context in which it appears.

Type inference and kind-preserving unification determines appropriate kinds for classes. A default of * is assumed for any parts of an inferred kind that cannot be fully determined by the corresponding definitions.

Type Operators

In November 2007, GHC 6.8.1 introduced the language extension TypeOperators. The extension allows operator symbols to be used as type constructors and does not allow them to be used as type variables. It now also enables ExplicitNamespaces (see further below).

Kind Signatures

GHC 6.8.1 also introduced the language extension KindSignatures. The extension allows kind signatures to be added to type variables.

Data Kinds

In February 2012, GHC 7.4.1 introduced the language extension DataKinds. For certain datatypes of the kind * -> ... -> * -> *, the extension automatically created (1) a kind for every such datatype (with the same name) and (2) type constructors for every value constructor (with similar names, but preceded by ').

For example, with the extension, data Bool = True | False results in a kind Bool and type constructors 'True :: Bool and 'False :: Bool.

The extension also enables numeric and string literals at the type level. Numeric literals are of kind Nat and string literals are of kind Symbol – these datatypes/kinds are exported from module GHC.TypeLits of package base-4.6.0.0 and subsequent versions.

Module GHC.TypeLits

Poly Kinds

GHC 7.4.1 also introduced the language extension PolyKinds, which allowed kind polymorphic types. The extension was further developed in GHC 7.6.1 (September 2012). PolyKinds also enables KindSignatures.

For example, in GHCi 8.4.3:

With kind polymorphism enabled, the kind inferred is the most general one.

Constraint Kinds

GHC 7.4.1 also introduced the language extension ConstraintKinds. The extension introduced a kind Constraint. Anything that was already a valid constraint in a type signature was of kind Constraint and some new things were also of kind Constraint. Things of kind Constraint could be used as constraints.

The extension also enabled type constraint synonyms. For example:

Module GHC.Exts of package base-4.5.0.0 (associated with GHC 7.4.1) now exported the datatype/kind Constraint.

Explicit Namespaces

In September 2012, GHC 7.6.1 introduced the language extension ExplicitNamespaces. The extension allows the names of type constructors in export or import lists to be prefixed with type. The ability to separately identify type constructors is necessary if TypeOperators is enabled.

Type In Type

In May 2016, GHC 8.0.1 introduced the experimental language extension TypeInType, which declares that types and kinds are one and the same. This allows features such as explicit quantification over kind variables, higher-rank kinds and the use of type synonyms and families in kinds. TypeInType also enables DataKinds and PolyTypes.

Module Data.Kind of package base-4.9.0.0 exports * and Type as synonyms of the kind of nullary type constructors.

With TypeInType enabled, the symbol * is no longer available by default for the kind of nullary type constructors; it has to be expressly imported from module Data.Kind. This is illustrated in the example below.